A:Type, eq:EqDecider(A), f,g:fpf(A; x.top).
sqequal(fpf-is-empty(fpf-join(eq; f; g)); band(fpf-is-empty(f); fpf-is-empty(g))) 

latex

Definitions

x:A. B(x), fpf-is-empty(f), fpf-join(eq; f; g), t.1, fpf-dom(eq; x; f), t  T, x. t(x), (i = j), ||as||, append(as; bs), b, deq-member(eq; x; L), band(p; q), Y, reduce(f; k; as), ff, if b then t else f fi , tt, l_all(L; T; x.P(x)), b, x(s), P  Q, True, P  Q, P  Q, T, prop{i:l}, P  Q, fpf(A; a.B(a)), sq_type(T), guard(T), , Unit,

Lemmas

bool sq, fpf wf, top wf, deq wf, filter trivial, btrue wf, eq int wf, length wf1, l member wf, bool wf, squash wf, true wf, add functionality wrt eq, append wf, filter wf, bnot wf, bor wf, eqof wf, deq-member wf, length append, band wf, iff transitivity, assert wf, eqtt to assert, assert of eq int, non neg length, not wf, eqff to assert, assert of bnot, not functionality wrt iff, filter functionality, bnot thru bor, bfalse wf